(set-info :smt-lib-version 2.6)
(set-logic QF_AX)
(set-info :status unsat)
(declare-sort Index 0)
(declare-sort Element 0)
(declare-fun a () (Array Index Element))
(declare-fun i () Index)
(declare-fun j () Index)
(declare-fun e () Element)
(declare-fun b () Bool)
(assert (not (= i j)))
(assert (or b (not (= (select a j) (select (store a i e) j)))))
(assert (or (not b) (not (= (select a j) (select (store a i e) j)))))
(check-sat)
(exit)
